T:Type, as,bs:(T List), a,b:T.
compat(T; cons(a; as); cons(b; bs))  ((a = b)  compat(T; as; bs)) 

latex

Definitions	t  T, x:A. B(x), compat(T; l1; l2), prop{i:l}, P  Q, P  Q, P  Q, P  Q, P  Q, iseg(T; l1; l2), guard(T)
Lemmas	iseg wf, cons iseg, compat wf